#include <pthread.h>

#include "predicates.h"
#include "prover.h"
#include "system.h"
#include "tuple.h"

struct SpawnParameters {
  pNode toProve;
  System *system;
};

void *spawned (void *passedIn) {
  SpawnParameters *params = (SpawnParameters*) passedIn;

  // Uses a new trail
  Trail trail;
  System system (params->system->rules, params->system->globals, trail);
  Prover *prover = Prover::create (*params->toProve, system);
  prover->prove ();
  delete params;
  delete prover;

  return 0;
}

// Note: do not pass any unbinded variables to/from the spawned query. Two
//  threads may bind into the same variable and the behaviour is undefined
class spawn : public OnceBindTupleProver {
predicateName("spawn")

  bool proveOnce () {
    SpawnParameters *params = new SpawnParameters;
    params->toProve = excludeFirst (*tuple).node->replicate ();
    params->system = system;

    pthread_t thread;
    return pthread_create (&thread, 0, spawned, params) == 0;
  }
};

ProverFactoryRegistrar<spawn, Tuple::ID> spawnRegistrar;
